$\forall$$A$:Type\{j\}, $B$:($A$$\rightarrow$Type\{i\}), $x$:$A$, $v$:$B$($x$). fpf{-}single($x$; $v$) $\in$ fpf($A$; $x$.$B$($x$))